M.ef(k,x,s,v,w) == E != 1of(2of(2of(2of(2of(M)))))(<k,x>)  w = E(s,v) 

latex

---

clarification:

M.ef(k,x,s,v,w)
== fpf-val(product-deq(Knd;Id;KindDeq;IdDeq);
== fpf-val(1of(2of(2of(2of(2of(M)))));
== fpf-val(<k,x>;
== fpf-val(kx,E.(w = E(s,v)  M.ds(x))) 

latex

Definitions	z != f(x)  P(a;z), product-deq(A;B;a;b), Knd, Id, KindDeq, IdDeq, 1of(t), 2of(t), M.ds(x)
FDL editor aliases	ma-ef